\begin{tabbing}
es{-}leaks(${\it es}$;$e$;$x$;${\it e'}$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\exists$\=$a$:Atom1\+
\\[0ex](es{-}atom(${\it es}$;es{-}loc(${\it es}$; $e$);$a$)
\\[0ex]\& (\=$\neg$free{-}from{-}atom\{1\}(es{-}state{-}without(${\it es}$;es{-}loc\+
\\[0ex](${\it es}$; $e$);$x$);es{-}state{-}when{-}without(${\it es}$;$e$;$x$);$a$))
\-\\[0ex]\& es{-}rcv{-}atom(${\it es}$;$e$;$a$)
\\[0ex]\& (\=($\uparrow$es{-}isrcv(${\it es}$; ${\it e'}$))\+
\\[0ex]c$\wedge$ \=(es{-}sender(${\it es}$; ${\it e'}$) = $e$ $\in$ es{-}E(${\it es}$)\+
\\[0ex]\& ($\neg$free{-}from{-}atom\{1\}(es{-}valtype(${\it es}$; ${\it e'}$);es{-}val(${\it es}$; ${\it e'}$);$a$)))))
\-\-\-
\end{tabbing}